(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v13 () Bool)
(declare-fun v14 () Bool)
(declare-fun v15 () Bool)
(declare-fun v16 () Bool)
(declare-fun v17 () Bool)
(assert (let ((e18 
(and
 (or (not v4) (not v2) (not v6))
 (or (not v2) (not v4) v7)
 (or v1 (not v15) (not v2))
 (or (not v1) v1 (not v14))
 (or (not v3) v6 (not v14))
 (or v8 (not v3) (not v11))
 (or v8 v11 (not v1))
 (or v16 (not v4) v5)
 (or (not v6) (not v9) (not v17))
 (or (not v7) v5 v17)
 (or (not v1) (not v6) v8)
 (or v1 (not v8) v16)
 (or v15 (not v7) v3)
 (or (not v3) v3 v5)
 (or v7 (not v6) (not v6))
 (or v5 v7 (not v7))
 (or v6 v8 (not v9))
 (or v0 v14 (not v12))
 (or (not v13) v16 v1)
 (or (not v11) v0 v3)
 (or v10 (not v6) v8)
 (or (not v7) v9 v5)
 (or (not v4) v16 v17)
 (or (not v13) (not v2) v13)
 (or (not v8) v11 (not v9))
 (or (not v10) (not v16) v13)
 (or v0 v5 (not v6))
 (or v5 (not v3) v10)
 (or v3 (not v1) (not v11))
 (or v2 (not v10) v17)
 (or v6 v3 v12)
 (or (not v14) v13 (not v16))
 (or v11 v17 v9)
 (or v13 v12 (not v6))
 (or v0 v6 (not v1))
 (or v9 v9 (not v9))
 (or v11 (not v12) v4)
 (or v8 v11 v9)
 (or (not v11) (not v2) v1)
 (or v0 (not v4) (not v4))
 (or (not v4) (not v8) v15)
 (or v12 v9 (not v15))
 (or v3 (not v2) v15)
 (or (not v4) (not v3) (not v1))
 (or (not v2) (not v2) v16)
 (or v10 v15 v4)
 (or (not v8) (not v1) (not v2))
 (or (not v17) v11 v17)
 (or v1 v15 (not v3))
 (or v15 (not v10) (not v8))
 (or (not v2) v5 v6)
 (or v8 v17 v14)
 (or v5 (not v2) (not v3))
 (or (not v17) v7 v12)
 (or v10 v11 (not v5))
 (or (not v11) (not v7) v14)
 (or (not v0) (not v10) v3)
 (or (not v0) (not v6) v10)
 (or (not v8) (not v11) (not v16))
 (or v11 v14 (not v15))
 (or (not v14) (not v15) (not v6))
 (or v17 v4 (not v16))
 (or v16 (not v16) v2)
 (or v4 v5 v8)
 (or (not v13) v12 v16)
 (or v16 (not v14) v4)
 (or v6 (not v17) (not v2))
 (or v15 (not v11) v10)
 (or v1 v2 (not v6))
 (or v10 v2 v13)
 (or (not v5) (not v13) (not v15))
 (or (not v9) v16 (not v13))
 (or (not v7) (not v9) v3)
 (or v13 (not v11) v9)
 (or (not v14) (not v0) (not v2))
 (or v11 (not v9) v7)
 (or v13 (not v1) (not v14))
 (or v9 (not v9) (not v16))
 (or (not v13) v14 (not v12))
 (or (not v7) (not v6) v7)
 (or (not v9) (not v8) v3)
 (or (not v12) (not v11) (not v1))
 (or v11 v2 v16)
 (or (not v6) v6 v3)
 (or v15 v14 (not v15))
 (or (not v17) v16 v11)
 (or (not v3) (not v5) v15)
 (or (not v2) (not v7) (not v5))
 (or (not v1) v13 (not v9))
 (or v7 v8 (not v9))
)))
e18
))

(check-sat)
